Skip to content

Story 5.4b: the verdict algebra is total, and a gate refuses the float - #55

Merged
guycorbaz merged 5 commits into
masterfrom
story-5.4b-verdict-algebra-and-float-gate
Jul 30, 2026
Merged

Story 5.4b: the verdict algebra is total, and a gate refuses the float#55
guycorbaz merged 5 commits into
masterfrom
story-5.4b-verdict-algebra-and-float-gate

Conversation

@guycorbaz

Copy link
Copy Markdown
Owner

Closes the last piece of Epic 5's vocabulary work: the engine can now conclude. It still cannot observe — nothing produces a Verdict, so nothing calls decide outside its own tests.

What ships

  • decide(Vec<RuleVerdict>, RulesetVersion) -> Decision in identity/cascade.rs — D13's six-row table as a total pure function, plus the one input class the table leaves uncovered.
  • A sixth cargo xtask ci gate, float-free — reds on an f32, an f64 or a bare float literal in code under identity/. Comments are stripped, so the architecture may be quoted.
  • 271 → 280 tests (135 bin + 100 core + 45 xtask).

The design decision

decide returns a Decision, not a bare Conclusion. The returned verdict_vector is the input, and the named rule is selected from it — which makes "a conclusion naming a rule absent from its own vector" and "a Match with an empty vector" unreachable through the function rather than merely unenforced. That is the invariant story 5.4 registered as untestable at the type level. A struct literal built elsewhere is still free; that residue moved to story 5.9.

The arms are a match on a presence tuple, and that is load-bearing

Deleting the arbitration arm gives error[E0004]: non-exhaustive patterns: (false, false, false, true) not coveredthe compiler names the missing class. Validation had measured that an if-chain swallows the same deletion with all 16 classes keeping their answer, so the construct is binding rather than stylistic.

The arbitration

D13's table leaves exactly one class uncovered — ≥1 Opposes with no Decisive, no Supports, no Disqualifying. Guy's call, 2026-07-29: it abstains for absence of proof. Nothing argues for the merge, so there is no merge to refuse. The correction to D13's own table is a milestone act, never a story task — now issue #54.

Five mutations, two predictions corrected by measurement

predicted observed
M1 conflict arm's cause 2 of 32 2 of 32 ✓ — but only once the walk was made cumulative; a bare assert_eq! aborts on the first mismatch and hides the count
M2 delete arbitration arm E0004 E0004, naming the class ✓
M3 min()next() permutation reds, walk does not ✓ — confirms the walk gives the tiebreak zero coverage
M4 remove comment-stripping reds on 1 citation 47 offenders — the other 46 are story references (5.4b, 4.6a) which are literally digit-dot-digit, because the gate also catches bare literals
M5 a real float in code 1 red 2 — the type and the literal

One of the five reds is compiler-carried (M2); four are not. M5 was observed through cargo xtask ci's output rather than a test run, and saying so is the honest form.

Bookkeeping

Twelve doc locations corrected, found by grepping the final tree rather than from the story's list of five — three do not name 5.4b and would have been missed, chiefly AbsenceOfProof's doc, which read "nothing in the verdict set argues either way" while the arbitrated class it now serves carries an Opposes.

Eight register entries annotated across four sections. The four NoMatch annotation lines in the 4.6a/4.7a sections claimed "nothing decides which side an input falls on"decide falsifies that. The empty-vector-literals entry is closed by its own prediction being refuted: the literals compiled untouched, and its count was wrong (four sites, not six).

⚠️ One process defect, recorded rather than smoothed: the first mutation pass ran against an uncommitted baseline and restored with git checkout, which reverts to HEAD and destroyed the implementation. Re-applied, then committed before re-running. A mutation pass needs a committed baseline to restore to.

Gate

fmt clean · clippy --all-targets clean · clippy without --all-targets clean (the CI form) · 280 tests · xtask ci six gates green with ℹ views-hash STALE exit 0 (issue #50, not regenerated) · fixtures/ untouched · cargo doc the same three pre-existing warnings · epics.md and architecture.md verified and NOT edited.

🤖 Generated with Claude Code

guycorbaz and others added 5 commits July 29, 2026 23:44
Committed BEFORE running the prove-to-red mutations, deliberately: the first
attempt used `git checkout` to restore a mutation while the baseline was
uncommitted, which reverted to HEAD and destroyed the implementation. A
mutation pass needs a committed baseline to restore TO.

271 -> 280 tests (135 bin + 100 core + 45 xtask). xtask ci: six gates green.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`identity/cascade.rs` gains `decide(Vec<RuleVerdict>, RulesetVersion) -> Decision`
— D13's table as a TOTAL pure function — plus its private `smallest_rule_with`.
`xtask` gains a sixth gate, `float-free`. Six new core tests, three new xtask
tests. 271 -> 280 (135 bin + 100 core + 45 xtask).

NOTHING produces a Verdict, so nothing calls decide outside its own tests: no
rule, no join, no blocker, no persistence, no corpus wiring.

THE DESIGN. `decide` returns a Decision, not a bare Conclusion, so the returned
verdict_vector IS the input and the named rule is selected FROM it. That makes
"a conclusion naming a rule absent from its own vector" and "a Match with an
empty vector" unreachable THROUGH THE FUNCTION rather than merely unenforced —
the invariant story 5.4 registered as untestable. A struct literal built
elsewhere is still free; that residue moved to story 5.9.

THE ARMS are a `match` on the presence tuple, not an if-chain, and that is
load-bearing rather than stylistic: deleting the arbitration arm gives
`error[E0004]: non-exhaustive patterns: (false, false, false, true) not
covered` — the compiler NAMES the missing class. Validation had measured that
an if-chain swallows the same deletion with all 16 classes keeping their answer.

THE ARBITRATION. D13's six rows leave exactly one input class uncovered —
>=1 Opposes with no Decisive, no Supports, no Disqualifying. Guy's call of
2026-07-29: it abstains for absence of proof. The correction to D13's own table
is a MILESTONE act, never a story task, and is now GitHub issue #54.

FIVE mutations run. TWO predictions corrected BY MEASUREMENT:

- M1 (the conflict arm's cause) -> exactly 2 of 32 subsets. That count is only
  observable because the 32-walk was made CUMULATIVE: a bare assert_eq! inside
  the loop aborts on the first mismatch, so the first run reported one subset
  where two had moved. The difference between "M1 reds" and "M1 reds on exactly
  2 of 32" is the walk's coverage, measured.
- M4 (remove the comment-stripping) -> 47 offenders on the real tree, not 1.
  The other 46 are STORY REFERENCES in prose: `5.4b`, `4.6a`, `4.7a` are
  literally digit-dot-digit, because the gate also matches BARE float literals —
  `let confidence = 0.85;` carries no f32/f64 token at all and is the likeliest
  shape an invented weight takes. The stripping and the literal rule are
  load-bearing together, and the gate's doc now says so with the number.
- M2 -> error[E0004]. M3 (min -> next) -> ONLY the permutation test reds, the
  32-walk stays green, confirming that the walk gives the tiebreak zero
  coverage. M5 (a real float) -> 2 reds naming file and line, not 1.

ONE of the five reds is compiler-carried (M2) and four are not. M5 was observed
through `cargo xtask ci`'s output rather than a test run, and saying so is the
honest form. Story 5.4's record claimed two of four were assertion-carried when
only one was; this is the corrected shape.

TWELVE doc locations corrected, found by grepping the final tree rather than
from the story's list of five. Three do not name 5.4b and that list would have
missed them — chiefly AbsenceOfProof's doc, which read "nothing in the verdict
set argues either way" while the arbitrated class it now serves carries an
Opposes. The gap-hunt validation agent caught that one before dev.

REGISTER: eight entries annotated across four sections (validation corrected
"six in one"). The four NoMatch annotation lines in the 4.6a/4.7a sections said
"nothing decides which side an input falls on" — decide falsifies that, and the
Outcome-mapping half moves to 5.7. The empty-vector-literals entry is closed by
its own prediction being REFUTED: the literals compiled untouched, and its count
was wrong (four sites, not six). A new section opens nine items: six name a
story, two name a condition, one names a milestone; one of the six also names
Epic 6. Counted after the last edit — a first draft of that preamble summed to
nine only by counting the epic as an item and forgetting the milestone.

⚠️ ONE PROCESS DEFECT, recorded because it cost the implementation once: the
first mutation pass ran against an UNCOMMITTED baseline and restored with
`git checkout`, which reverts to HEAD and wiped decide and its tests. Re-applied,
then committed before re-running. A mutation pass needs a committed baseline to
restore TO — the story's warning named the symptom, not the mechanism.

Gate run whole: fmt clean; clippy --all-targets clean; clippy WITHOUT
--all-targets clean (the CI form); 280 tests; xtask ci six gates green with
views-hash STALE exit 0 (issue #50, NOT regenerated); fixtures/ untouched;
cargo doc the same three pre-existing warnings. epics.md and architecture.md
verified and NOT edited.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tokenises

Applies the code half of the 2026-07-30 three-layer review (22 patch items,
1 decision resolved by Guy, 5 deferrals registered).

decide() now matches on (Option<RuleId>, Option<RuleId>, bool, bool) as AC1
prescribed, so the presence test and the rule selection are one act and the two
unreachable arms are gone rather than justified — they had mapped an impossible
state onto Abstained{AbsenceOfProof}, a legitimate answer for two other classes.
Exhaustiveness survives: deleting the arbitration arm is still error[E0004].

The float gate's matcher is a numeric-literal tokeniser instead of a
digit-dot-digit search plus a substring test. Measured before: 1e-3 and 1. were
GREEN (both f64), while "192.168.0.1", t.0.1 and a_f64_never_decides() were RED.
All five now answer correctly. The comment stripper tracks string literals, so a
// inside a string no longer hides the code after it. The gate also fails closed
on a guarded directory that holds no .rs file, and sorts its offenders.

Doc corrections, each of which asserted something checkable and wrong: the doc
table's last row named NoMatch where decide returns Abstained; the tiebreak was
called semantically empty when byte order prefers l1-* over l2-* and flips at
l10-; Decision closed "no explanation" over the empty VECTOR, not empty
evidence; subset()'s scrambled NAMES were justified by a property its own test
cannot have; and a test doc claimed the D13 citation was the workspace's only
f64 token (there are 22) while its premise guard had gone inert.

Removed one assertion that could not fail (decide called twice, outputs compared)
and derived the totality walk's bound from Verdict::all() so a sixth variant
cannot halve the coverage in silence.

280 -> 281 tests (135 bin + 100 core + 46 xtask). Six gates green, both clippy
forms clean. Bookkeeping counts are corrected in a follow-up commit, after this
tree is the one they describe.
Halving the derived bound was measured to leave all 100 core tests green: the
oracle agrees on every class the walk still visits, so 'every input class' was
asserted by nothing. Asserting that each Verdict variant appeared in some walked
subset reds on that mutation (Disqualifying is the highest bit).

Recorded because it cost the same mistake twice: this assertion was written,
proven, and then destroyed by a git checkout restoring to HEAD during the
mutation pass — the process defect story 5.4b itself documented.
Applies the record half of the 2026-07-30 code review. Seven of its eight HIGH
findings were about claims rather than behaviour, and this commit is where those
claims stop being wrong.

  47 offenders           -> 45 under the matcher that shipped, and 42 once this
                            review replaced it with a tokeniser. Three values for
                            one sentence inside one story, which is the argument
                            for asserting instead of quoting: no figure is written
                            in code now, a test asserts the gap.
  EIGHT register entries -> TEN. grep -c gives 10; the sentence that said eight
                            enumerated ten in its own next clause.
  TWELVE doc locations   -> TEN doc blocks. Twelve was reachable only by excluding
                            the xtask module doc that Task 6 itself lists.
  three sentences left   -> ONE pre-existing sentence; the others were written by
                            the story, not left by it.
  M5's "2 reds"          -> withdrawn. line_has_float returns on the first match,
                            so the gate pushes at most one offender per line; the
                            mutation text was never recorded.
  project-context.md     -> 281 tests (135+100+46) and the falsified sentence
                            rewritten. Task 9's checkbox had been the claim.
  "four real gates"      -> six. file-size and float-free had both shipped without
                            this sentence being updated.

The register gets its missing annotation: lib.rs's flat re-export entry still said
five names while decide made six, and 5.4b's File List claimed that cost was
recorded. Appended, never rewritten, per AC8. Its :52 citation is corrected to :53
the same way — one bullet after AC8 says not to cite by line number.

PR #55 is now recorded in the story, sprint-status and CLAUDE.md; every
predecessor named its PR and this one named none.

Status stays `review`, not `done`: in this project `done` is the merge's business,
which is the convention story 5.1 recorded and the review workflow's default would
have broken.

281 tests, six gates green, both clippy forms clean, fixtures untouched,
architecture.md and epics.md untouched.
@guycorbaz
guycorbaz merged commit 4f4e774 into master Jul 30, 2026
1 check passed
@guycorbaz
guycorbaz deleted the story-5.4b-verdict-algebra-and-float-gate branch July 30, 2026 11:22
guycorbaz added a commit that referenced this pull request Jul 30, 2026
Bookkeeping only, no code. Brings the four documents that still said
`review` / "PR #55 open" to what `master` holds after `4f4e774`.

- story file `Status: review` → `done`
- `sprint-status.yaml`: the `5-4b-…` key → `done`, `last_updated`, and a
note on why `done` waited for the merge
- `CLAUDE.md` and `docs/project-context.md`: 5.4b `done`, and the next
step named as 5.5 (the L1 join, first caller of `decide`)

## Why `done` waited

`done` is the merge's business here, so 5.4b stayed at `review` through
its whole code review and its 22 patches. The review workflow's own step
6 would have set `done` as soon as the patches were applied; that
default was deliberately not followed, because it marks a story done
while its PR is still open. The deviation is recorded in the sprint
block rather than left implicit.

## State on master

281 tests (135 bin + 100 core + 46 xtask) · six `cargo xtask ci` gates
green · `ℹ views-hash STALE` exits 0 by design (issue #50, still owed at
a milestone).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01HEE7mz4xufqYW5xKfgJBaF
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant